Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	dx(X)	→ one
2:	dx(a)	→ zero
3:	dx(plus(ALPHA,BETA))	→ plus(dx(ALPHA),dx(BETA))
4:	dx(times(ALPHA,BETA))	→ plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
5:	dx(minus(ALPHA,BETA))	→ minus(dx(ALPHA),dx(BETA))
6:	dx(neg(ALPHA))	→ neg(dx(ALPHA))
7:	dx(div(ALPHA,BETA))	→ minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two))))
8:	dx(ln(ALPHA))	→ div(dx(ALPHA),ALPHA)
9:	dx(exp(ALPHA,BETA))	→ plus(times(BETA,times(exp(ALPHA,minus(BETA,one)),dx(ALPHA))),times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))

There are 12 dependency pairs:

The approximated dependency graph contains one SCC: {10-21}.

Consider the SCC {10-21}. There are no usable rules. By taking the AF π with π(DX) = π(ln) = π(neg) = 1 together with the lexicographic path order with empty precedence, the rules in {16,19} are weakly decreasing and the rules in {10-15,17,18,20,21} are strictly decreasing. There is one new SCC.
- Consider the SCC {16,19}. By taking the AF π with π(DX) = π(ln) = 1 together with the lexicographic path order with empty precedence, rule 19 is weakly decreasing and rule 16 is strictly decreasing. There is one new SCC.
  - Consider the SCC {19}. By taking the AF π with π(DX) = 1 together with the lexicographic path order with empty precedence, rule 19 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.03 seconds) --- May 3, 2006